Nuprl Lemma : int_inc_rationals
11,40
postcript
pdf
subtype(
; rationals)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
subtype(
S
;
T
)
Lemmas
int-rational
origin
; rationals) ; rationals) 
T
x:A. B(x)